Example 14 in [ Lucas - IC'06]

Summary: Ex14_Luc06

• TPDB format
• OBJ format
• Negative results:
  1. Lucas'
  2. Ferreira and Ribeiro's transformation
  3. Zantema's transformation
• Positive results:

Ex14_Luc06 in TPDB format ( Ex14_Luc06.trs):

(VAR X)
(STRATEGY CONTEXTSENSITIVE 
  (h 1)
  (g 1)
  (a)
  (f 1)
  (b)
)
(RULES 
h(X) -> g(X,X)
g(a,X) -> f(b,X)
f(X,X) -> h(a)
a -> b
)

The CS-TRS in OBJ format (file Ex9_Luc06.obj):

obj Ex14_Luc06 is
  sort S .
  op h : S -> S .
  op g : S S -> S [strat (1 0)] .
  op a : -> S .
  op f : S S -> S [strat (1 0)] .
  op b : -> S .
  vars X : S .
  eq h(X) = g(X,X) .
  eq g(a,X) = f(b,X) .
  eq f(X,X) = h(a) .
  eq a = b .
endo

Negative results

1. The µ-termination of Ex4_Luc06 cannot be proved by using Lucas' transformation. The TRS Ex14_Luc06_L:

   	h(X) -> g(X)
   	g(a) -> f(b)
   	f(X) -> h(a)
   	a -> b
   
   	
   

   is not terminating (AProVE).
   
2. The µ-termination of Ex14_Luc06 cannot be proved by using Ferreira and Ribeiro's or Zantema´s transformation. The transformed TRS Ex14_Luc06:

   						
   	h(X) -> g(X,X)
   	g(a,X) -> f(b,activate(X))
   	f(X,X) -> h(a)
   	a -> b
   	activate(X) -> X
   
   

   is not terminating (AProVE).
   

Positive results